$\forall$$T$, ${\it T'}$:Type, $x$:$T$, $a$:Atom1.
\\[0ex]AtomFree(Type;$T$) $\Rightarrow$ AtomFree(Type;${\it T'}$) $\Rightarrow$ $x$:$T$$>>$$a$ $\Rightarrow$ inl($x$):$T$+${\it T'}$$>>$$a$